package com.googlecode.kipler.satisfiability.completion.rule.formula;

import com.googlecode.kipler.container.dl.FormulaCategory;
import com.googlecode.kipler.container.dl.World;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.completion.rule.CompletionRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.uniformnotation.OrBetaFormula;
import com.googlecode.kipler.satisfiability.reasoner.Reasoner;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;


/**
 * IMPORTANT: This rule does not have a recursive method to handle multiple
 * levels of disjunctive formulae. It is because each application of the rule
 * branches the tableau tree.
 * 
 * @author İnanç Seylan
 * 
 */
public class OrRule extends CompletionRule {

	private BetaFormulaRule betaRule;

	public OrRule(Reasoner reasoner) {
		betaRule = new BetaFormulaRule(reasoner, FormulaCategory.OR,
				new OrBetaFormula(), false, "Or rule");
	}

	public void apply() throws ReasonerException {
		betaRule.apply();
	}

	public WorldConstraintSystem getWcs() {
		return betaRule.getWcs();
	}

	public World getWorld() {
		return betaRule.getWorld();
	}

	public boolean isApplied() {
		return betaRule.isApplied();
	}

	public void setWcs(WorldConstraintSystem wcs) {
		betaRule.setWcs(wcs);
	}

	public void setWorld(World world) {
		betaRule.setWorld(world);
	}
	
	

}
